A, B:Type, a:EqDecider(A), b:EqDecider(B), p, q:A+B. p = q  sumdeq(a;b)(p,q) 

latex

Definitions	A, t  T, Prop, False, P  Q, x:A. B(x), P & Q, P  Q, P  Q, b, EqDecider(T), sumdeq(a;b), P  Q, Dec(P)
Lemmas	decidable false, deq wf, false wf, assert wf